Lambda the Ultimate

Polymorphic Delimited Contiunations by Kenichi Asai and Yukiyoshi Kameyama, in the 5^th ASIAN Symposium on Programming Languages and Systems (2007).

This paper presents a polymorphic type system for a language with delimited control operators, shift and reset. Based on the monomorphic type system by Danvy and Filinski, the proposed type system allows pure expressions to be polymorphic. Thanks to the explicit presence of answer types, our type system satisfies various important properties, including strong type soundness, existence of principal types and an inference algorithm, and strong normalization. Relationship to CPS translation as well as extensions to impredicative polymorphism are also discussed. These technical results establish the foundation of polymorphic delimited continuations.

Now, the real reason that I post this is because of Oleg's ShiftResetGenuine, which implements polymorphic delimited continuations in Haskell, and primarily cites this paper as well as Robert Atkey's Parameterized Notions of Computation. So if you find this paper challenging to read, Oleg provides you with a concrete playground in which to experiment.

It's also notable that Matthieu Sozeau has GenuineShiftReset available, which is a Coq version of Oleg's code.

2009 Lang.NET videos are available here

Some of the speakers include:
Lars Bak (Google Chrome Javascript VM)
Gilad Bracha
Anders Hejlsberg
Erik Meijer
John Rose (JVM)
Philip Wadler

A Generic Type-and-Effect System

Type-and-effect systems are a natural approach for statically reasoning about a program's execution. They have been used to track a variety of computational effects, for example memory manipulation, exceptions, and locking. However, each type-and-effect system is typically implemented as its own monolithic type system that hard-codes a particular syntax of effects along with particular rules to track and control those effects. We present a generic type-and-effect system, which is parameterized by the syntax of effects to track and by two functions that together specify the effect discipline to be statically enforced. We describe how a standard form of type soundness is ensured by requiring these two functions to obey a few natural monotonicity requirements. We demonstrate that several effect systems from the literature can be viewed as instantiations of our generic type system. Finally, we describe the implementation of our type-and-effect system and mechanically checked type soundness proof in the Twelf proof assistant.

Things really seem to be heating up in both the type-and-effects world and the mechanized metatheory world (but then, long-time LtU readers will expect me to claim that, won't they)? Of course, I also have my usual question as to what aspects of Twelf these researchers found helpful to their constructions vs. those of Coq.

Generic Discrimination: Sorting and Partitioning Unshared Data in Linear Time, Fritz Henglein. ICFP 2008.

We introduce the notion of discrimination as a generalization of both sorting and partitioning and show that worst-case linear-time discrimination functions (discriminators) can be defined generically, by (co-)induction on an expressive language of order denotations. The generic definition yields discriminators that generalize both distributive sorting and multiset discrimination. The generic discriminator can be coded compactly using list comprehensions, with order denotations specified using Generalized Algebraic Data Types (GADTs). A GADT-free combinator formulation of discriminators is also given.

We give some examples of the uses of discriminators, including a new most-significant-digit lexicographic sorting algorithm.

Discriminators generalize binary comparison functions: They operate on n arguments at a time, but do not expose more information than the underlying equivalence, respectively ordering relation on the arguments. We argue that primitive types with equality (such as references in ML) and ordered types (such as the machine integer type), should expose their equality, respectively standard ordering relation, as discriminators: Having only a binary equality test on a type requires Θ(n^2) time to find all the occurrences of an element in a list of length n, for each element in the list, even if the equality test takes only constant time. A discriminator accomplishes this in linear time. Likewise, having only a (constant-time) comparison function requires Θ(n log n) time to sort a list of n elements. A discriminator can do this in linear time.

If you're like me, at some point you probably heard about linear time sorts like radix sort and then dismissed them as an interesting curiosity --- the restriction to sorting numbers seems pretty limiting, after all.

Henglein did not, and in this paper he shows how to write a teeny-tiny library of type-directed combinators that can lift linear time sorts to structured types like lists and trees, and in addition lets you quotient out by order or repetition, if you want. It's terrifically pretty code.

Note: This is a link to the ACM digital library, and so is behind a paywall. I found a link to a tech report by Henglein covering the same material, but I don't exactly what is different.

In Semantics of Memory Management for Polymorphic Languages (1997) Greg Morrisett and Robert Harper

...present a static and dynamic semantics for an abstract machine that evaluates expressions of a polymorphic programming language. Unlike traditional semantics, our abstract machine exposes many important issues of memory management, such as value sharing and control representation. We prove the soundness of the static semantics with respect to the dynamic semantics using traditional techniques. We then show how these same techniques may be used to establish the soundness of various memory management strategies, including type-based, tag-free garbage collection; tail-call elimination; and environment strengthening.

This should keep the formal semantics LtUers happy for a little while. But is all the machinery necessary? Is there an easier way to prove that garbage can be thrown out?

This blog post about Idris led me to Edwin C. Brady's 2005 PhD thesis, Practical Implementation of a Dependently Typed Functional Programming Language.

This thesis considers the practical implementation of a dependently typed programming language, using the Epigram notation defined by McBride and McKinna. Epigram is a high level notation for dependently typed functional programming elaborating to a core type theory based on Luo's UTT, using Dybjer's inductive families and elimination rules to implement pattern matching. This gives us a rich framework for reasoning about programs. However, a naive implementation introduces several run-time overheads since the type system blurs the distinction between types and values; these overheads include the duplication of values, and the storage of redundant information and explicit proofs.

A practical implementation of any programming language should be as efficient as possible; in this thesis we see how the apparent efficiency problems of dependently typed programming can be overcome and that in many cases the richer type information allows us to apply optimisations which are not directly available in traditional languages. I introduce three storage optimisations on inductive families; forcing, detagging and collapsing. I further introduce a compilation scheme from the core type theory to G-machine code, including a pattern matching compiler for elimination rules and a compilation scheme for efficient runtime implementation of Peano's natural numbers. We also see some low level optimisations for removal of identity functions, unused arguments and impossible case branches. As a result, we see that a dependent type theory is an effective base on which to build a feasible programming language.

What's the current state of the art in optimization of dependently typed languages?

Last year, Ehud said the only reason he missed the Scala Lift Off was because it didn't have enough marketing. So this year I'm spam^h^h^h^h posting it on the LtU front page.

The Scala Lift Off San Francisco will be held on Saturday, June 6th in San Francisco. This is the Saturday after JavaOne. Admission to the event is $200. If you are a full time student or faculty member, the cost is $50. We'll have hot and cold running food and beverages, improved wifi, and lots of terrific members of the Scala and Lift community.

Further details and registration are at the conference site. I'll add comments to this topic as more information becomes available.

For some inexplicable reason COBOL doesn't get much love from LtU. But COBOL turns 50 some time this year and we owe a tip of the hat to this venerable language behind so many large institutions.

The Guardian understands.

According to Michael Coughlan, a lecturer at the University of Limerick, one of Cobol's perceived drawbacks is its verbosity. But he reckons that's also one of its strengths. "It's not just a write-only language," he says. "You can come back years later and understand the code."

This opinion is shared by Mike Gilpin, of Forrester, who is an ex-Cobol programmer. "Cobol is one of the few languages written in the last 50 years that's readable and understandable," he says. And he's scathing about the readability of more fashionable languages, such as PHP and Java: "Modern programming languages are ridiculously hard to understand."

There you have it! More readable than PHP and Java. A ringing endorsement for the next half century.

Philipp Haller and Martin Odersky have submitted Capabilities for External Uniqueness to OOPSLA'09.

Unique object references have many important applications in object-oriented programming. For instance, with sufficient encapsulation properties they enable safe and efficient transfer of message objects between concurrent processes. However, it is a long-standing challenge to integrate unique references into practical object-oriented programming languages.

This paper introduces a new approach to external uniqueness. The idea is to use capabilities for enforcing both aliasing constraints that guarantee external uniqueness, and linear consumption of unique references. We formalize our approach as a type system, and prove a type preservation theorem. Type safety rests on an alias invariant that builds on a novel formalization of external uniqueness.

We show how a capability-based type system can be used to integrate external uniqueness into widely available object-oriented programming languages. Practical experience suggests that our system allows adding uniqueness information to common collection classes in a simple and concise way.

A prototype plugin for the Scala compiler can be found on the same page.

In an email to the BitC developer mailing list Jonathon Shapiro announced that he is wrapping up development on BitC.

Some of you will have noticed that I have been conspicuously silent over the
last three or four weeks. I have spent much of that time airborne, or in
interviews at Google, Microsoft, and DARPA.

After a fair bit of soul-searching, I have decided to accept a fairly senior
position at Microsoft associated with the Midori project. The current plan
has me starting there at the beginning of August.

This means, among other issues, that we will be wrapping up the BitC
project. While I will be trying hard to get all of the planned features for
the initial release completed before I depart, that may not turn out to be
possible. I have asked Microsoft if we can keep the various web sites alive
for archival access and the mailing list, but I should also ask if there is
anyone out there who would be interested to assume more active stewardship
of the BitC project. I emphasize that unless management at Microsoft
concludes otherwise, I will no longer be able to participate actively in
these discussions. Also, in the event that MS does not permit archival
maintainence, would somebody be willing to take over hosting the content?

I have also asked MS for permission to publish papers about BitC on my own
time. They granted this permission to Swaroop, and I see no reason that they
should decline this, but my position there is a bit more sensitive and they
may see issues that I do not.

In the meantime, I need to get back to packing and hacking.

Best regards,

Jonathan

Best of luck shap! And best of luck BitC!